FDL - Nuprl Lemma : can-apply-fun-exp

Nuprl Lemma : can-apply-fun-exp

A:Type, f:(A

(A + Top)), n:

can-apply(f^n;y))

can-apply(f^m;y)))

Definitions	t T, x:A. B(x), A B, -n, a < b, Void, x:AB(x), P Q, False, A, , {x:A\| B(x)} , , f^n, f o g , f(a), Top, isl(x), b, Type, , True, P Q, T, left + right, , x:A B(x), P & Q, P Q, {T}, SQType(T), p-id(), s = t, P Q, Dec(P), can-apply(f;x), i j , #$n, n - m, n+m, s ~ t, do-apply(f;x)
Lemmas	false wf, ge wf, nat properties, nat wf, top wf, decidable int equal, nat sq, bool wf, squash wf, true wf, p-fun-exp-add, assert wf, isl wf, p-compose wf, p-fun-exp wf, le wf